.TH YICES-SMT 1 "March 2020" "Yices 2.6.2" "User Commands"
.SH NAME
yices-smt \- the Yices SMT solver for the SMT-LIB 1.2 language
.SH SYNOPSIS
.B yices-smt
[
.I options
]
[
.I file
]
.SH DESCRIPTION
Runs the Yices SMT solver on an input problem written in SMT-LIB 1.2.
If no
.I file
is given, the problem is read from standard input.
.P
SMT-LIB 1.2 is the old version of the SMT-LIB language. It was replaced
by SMT-LIB 2.0 in 2012.
.
.SH OPTIONS
.TP
.B \-\-version,  \-V
Display version and exit.
.TP
.B \-\-help,  \-h
Display a short help summary.
.TP
.B \-\-model,  \-m
Print a model (on stdout) if the problem is satisfiable (some variables may be eliminated).
.TP
.B \-\-full\-model\fR,  \-f
Print a full model if the problem is satisfiable. This gives more details than option
\fB\-\-model\fR.
.TP
.B \-\-verbose,  \-v
Print statistics and other data during the search.
.TP
.B \-\-stats,  \-s
Print a statistics summary at the end of the search.
.TP
.BI \-\-timeout= timeout, \& "" \-t "" " " timeout
Give a
.I timeout
in seconds. There is no timeout by default.
.
.SH SEE ALSO
.BR yices (1),
.BR yices-sat (1),
.BR yices-smt2 (1)
.PP
For bug reporting and other information, please visit http://yices.csl.sri.com.
.
.SH AUTHORS
.PP
Copyright (C) SRI International.
.PP
Yices is developed at SRI's Computer Science Laboratory. The main
developers are Bruno Dutertre <bruno@csl.sri.com>, Dejan Jovanovic
<dejan@csl.sri.com>, Ian A. Mason <iam@csl.sri.com>, and Stephane
Graham-Lengrand <stephane.graham-lengrand@sri.com>.
